The relentless increase in the number of transistors integrated on a single electronic chip has made the traditional method of chip verification using simulation more and more difficult and time-consuming. Desiring additional measures of design confidence, chip developers are increasingly turning to other methods of verification to augment simulation.
Formal verification delivers mathematical proofs of correctness without requiring simulation test bench development. Formal verification processes properties defining intended behavior and makes use of constraints that specify legal input values for the design. Properties can be defined by the chip designer in the form of assertion statements. Properties can also be automatically extracted by electronic design automation (EDA) tools. Verification properties often define relationships between signals on different cycles, e.g., if there is a request on cycle N, there should be an acknowledge generated on cycle N+1. To correctly model the environment of a design, designers specify constraints in SystemVerilog assertion (SVA), probabilistic soft logic (PSL), or other standard constraint language formats. The constraints are often referred to as ‘assumptions’ while the properties to be verified are called ‘assertions’.
To prove the correctness of a property, the verification tool often needs to check that one or more parts of the design correctly transition through a sequence of states. In many situations it is computationally infeasible to verify properties starting at the power-on state. If the verification tool is given a constraint specifying a starting state, the verification tool can attempt to verify the property.
Multiple verification tools select initial states by analyzing simulation results. Seawright et al. (U.S. Pat. No. 7,454,324) discuss such a verification tool. Before a logic designer can use such a tool, he or she must develop a simulation test bench, defining tests and test vectors. This takes considerable time and skill on the part of the logic designer in defining test vectors to aid verification.
Due to the intrinsic complexity of the hardware verification problem, existing formal verification tools can often give only an inconclusive ‘partial pass’ property verification result, meaning that the verification tool could neither prove nor disprove a property.
Logic designers would like to have a verification tool that gives more conclusive results, i.e., a verification tool that reports whether a property either passes or fails. Furthermore, logic designers would like to have a verification tool that does not require any simulation test bench.